(**
 * Type representation for types
 *
 * @copyright (C) 2021 SML# Development Team.
 * @author Atsushi Ohori
 *)
structure ReifiedTy =
struct

  exception ConSetNotFound
  exception GetConSetFail
  exception InstantiateFail
  exception GetConSetFail

  fun eqOpt (SOME x) y = x = y
    | eqOpt NONE y = true

  fun Undetermined string = raise Bug.Bug (string ^ " size undetremnined")

  (*%
     @formatter(BoundTypeVarID.id) BoundTypeVarID.format_id
   *)
  type btvId
    = (*% @format(id) "'" id *)
      BoundTypeVarID.id

  type typId = TypID.id

   (*%
    * @params(labelsep)
    * @formatter(list)  SMLFormat.BasicFormatters.format_list
    *)
   type  btvList =
     (*%
        @format(field fields)
          fields(field)(","+1) 
        @format:field(label * elem) label
      *)
     (btvId * btvId) list

  fun formatBtvenv (labelsep) env =
      format_btvList(labelsep) (BoundTypeVarID.Map.listItemsi env)

  (*%
     @formatter(SEnv.map) TermPrintUtils.formatSEnvMap
   *)
  datatype taggedLayout 
    = (*% 
         @format({tagMap:tag map})
          !N0{ "TAGGED_RECORD{tagMap:{" 
                2[1 map(tag)(":") ] "}" 1 "}" }
       *)
      TAGGED_RECORD of {tagMap: int SEnv.map}
    | (*% 
          @format({tagMap: tag map, nullName:name})
          !N0{ "TAGGED_OR_NULL{tagMap:{" 
                2[1 map(tag)(":") ] "}," + "nullName:" name 1 "}" }
       *)
      TAGGED_OR_NULL of {tagMap: int SEnv.map, nullName: string}
    | (*% 
          @format({tagMap:tag map})
          !N0{ "TAGGED_TAGONLY{tagMap:{" 2[1 map(tag)(":") ] "}" 1 "}" }
       *)
      TAGGED_TAGONLY of {tagMap: int SEnv.map}
  fun taggedLayoutToString reifiedTy =
      SMLFormat.prettyPrint nil (format_taggedLayout reifiedTy)
  fun taggedLayoutEq (TAGGED_RECORD {tagMap=map1}, TAGGED_RECORD {tagMap=map2}) =
      SEnv.isEmpty
        (SEnv.mergeWith 
           (fn (SOME a, SOME b) => if a = b then NONE else SOME (SOME a,SOME b)
             | (SOME a, NONE) => SOME (SOME a, NONE)
             | (NONE, SOME b) => SOME (NONE, SOME b)
             | (NONE, NONE) => NONE
           )
           (map1,map2)
        )
    | taggedLayoutEq (TAGGED_OR_NULL {tagMap=map1, nullName = name1},
                      TAGGED_OR_NULL {tagMap=map2, nullName = name2}) =
      name1 = name2 andalso
      SEnv.isEmpty
        (SEnv.mergeWith 
           (fn (SOME a, SOME b) => if a = b then NONE else SOME (SOME a,SOME b)
             | (SOME a, NONE) => SOME (SOME a, NONE)
             | (NONE, SOME b) => SOME (NONE, SOME b)
             | (NONE, NONE) => NONE
           )
           (map1, map2)
        )
    | taggedLayoutEq(TAGGED_TAGONLY {tagMap=map1},TAGGED_TAGONLY {tagMap=map2}) =
      SEnv.isEmpty
        (SEnv.mergeWith 
           (fn (SOME a, SOME b) => if a = b then NONE else SOME (SOME a,SOME b)
             | (SOME a, NONE) => SOME (SOME a, NONE)
             | (NONE, SOME b) => SOME (NONE, SOME b)
             | (NONE, NONE) => NONE
           )
           (map1, map2)
        )
    | taggedLayoutEq _ = false

  (*%
     @formatter(SEnv.map) TermPrintUtils.formatSEnvMap
   *)
  datatype layout
    = (*%
         @format(taggedLayout)
           "LAYOUT_TAGGED(" taggedLayout ")"
       *)
      LAYOUT_TAGGED of taggedLayout
    | (*% 
          @format({wrap})
         "LAYOUT_ARG_OR_NULL{wrap:" wrap "}"
       *)
      LAYOUT_ARG_OR_NULL of {wrap: bool}
    | (*% 
          @format({wrap})
           "LAYOUT_SINGLE_ARG{wrap:" wrap  "}"
       *)
      LAYOUT_SINGLE_ARG of {wrap: bool}
    | (*% 
          @format({falseName})
           "LAYOUT_CHOICE{falseName:" falseName  "}"
       *)
      LAYOUT_CHOICE of {falseName: string}
    | (*% 
          @format  "LAYOUT_SINGLE"
       *)
      LAYOUT_SINGLE

  (* check this *)
  fun isBoxedLayout layout =
      case layout of
      LAYOUT_TAGGED _ => true
    | LAYOUT_ARG_OR_NULL  _ => true
    | LAYOUT_SINGLE_ARG _ => true
    | LAYOUT_CHOICE  _ => false
    | LAYOUT_SINGLE => false

  fun layoutToString reifiedTy =
      SMLFormat.prettyPrint nil (format_layout reifiedTy)
  fun layoutEq (LAYOUT_TAGGED taggedLayout1, LAYOUT_TAGGED taggedLayout2) = 
      taggedLayoutEq (taggedLayout1, taggedLayout2)
    | layoutEq (LAYOUT_ARG_OR_NULL{wrap=wrap1}, LAYOUT_ARG_OR_NULL{wrap=wrap2}) =
      wrap1 = wrap2
    | layoutEq (LAYOUT_SINGLE_ARG {wrap =wrap1}, LAYOUT_SINGLE_ARG {wrap =wrap2}) =
      wrap1 = wrap2
    | layoutEq (LAYOUT_CHOICE {falseName=name1}, LAYOUT_CHOICE {falseName=name2}) =
      name1 = name2
    | layoutEq (LAYOUT_SINGLE, LAYOUT_SINGLE) = true
    | layoutEq _ = false

  (*%
     @formatter(BoundTypeVarID.Map.map) formatBtvenv
     @formatter(BoundTypeVarID.id) BoundTypeVarID.format_id
     @formatter(TypID.id) TypID.format_id
     @formatter(btvenv) formatBtvenv
     @formatter(list) SMLFormat.BasicFormatters.format_list
     @formatter(option) TermPrintUtils.formatPrependedOpt
     @formatter(SEnv.map) TermPrintUtils.formatSEnvMap
     @formatter(recordTy) TermFormat.formatRecordTy
     @formatter(Symbol.longsymbol) Symbol.format_longsymbol
   *)
  datatype reifiedTy
    = (*% @format(arg) arg + "array" *)
      ARRAYty of reifiedTy
    | (*% @format "bool" *)
      BOOLty
    | (*% @format "bottom" *)
      BOTTOMty
    | (*% @format "boxed" *)
      BOXEDty
    | (*%  @format(tid) tid *)
      BOUNDVARty of btvId
    | (*% @format "char" *)
      CHARty
    | (*% @format "codeptr" *)
      CODEPTRty
    | (*% 
         @format({longsymbol, id, args:ty tys, conSet, layout, size}) 
           tys(ty)(",") + longsymbol "(" id ")" 
           2[1 conSet]
           2[1 layout]
       *)
      CONSTRUCTty of {longsymbol: Symbol.longsymbol, 
                      id:TypID.id, 
                      args: reifiedTy list,
                      conSet : conSet,
                      layout: layout,
                      size : int
                     }
    | (*% 
         @format({longsymbol, id, args:ty tys, layout, size}) 
           tys(ty)(",") + longsymbol "(" id ")" 
           + 2[1 "datatype layout:" layout]
       *)
      DATATYPEty of {longsymbol: Symbol.longsymbol, 
                     id:TypID.id, 
                     args: reifiedTy list,
                     layout: layout,
                     size : int
                    }
    | (*% @format({boxed,size}) "?DummyTy"*)
      DUMMYty of {boxed : bool, size : word}
    | (*% @format({boxed,size,id}) "EXISTty(" id ")" *)
      EXISTty of {boxed : bool option, size : word option, id : int}
    | (*% @format(ty) ty + "dyn" *)
      DYNAMICty of reifiedTy
    | (*% @format "?ERRORty" *)
      ERRORty
    | (*% @format "exntag" *)
      EXNTAGty
    | (*% @format "exn" *)
      EXNty
    | (*% @format(arg args * resultTy)
            "{" args(arg)(",") + "}} -> " + resultTy
      *)
      FUNMty of reifiedTy list * reifiedTy
    | (*% @format(arg) arg + "IEnv.map" *)
      IENVMAPty of reifiedTy
    | (*% @format "int" *)
      INT32ty
    | (*% @format "int16" *)
      INT16ty
    | (*% @format "int64" *)
      INT64ty
    | (*% @format "int8" *)
      INT8ty
    | (*%  @format "internalTy"  *)
      INTERNALty
    | (*% @format "intInf" *)
      INTINFty
    | (*% @format(arg) arg + "list" *)
      LISTty of reifiedTy
    | (*% 
         @format({longsymbol, id, args:ty tys, boxed, size}) 
           tys(ty)(",") + longsymbol "(" id ")" 
       *)
      OPAQUEty of {longsymbol: Symbol.longsymbol, 
                   id:TypID.id, 
                   size : int,
                   boxed : bool,
                   args: reifiedTy list
                  }
    | (*% @format(arg) arg + "option" *)
      OPTIONty of reifiedTy
    | (*% 
         @format({boundenv:btv env, body:ty}) 
         "["env(btv)(",") "." + ty "]"
       *)
      POLYty of {boundenv: btvId BoundTypeVarID.Map.map, body: reifiedTy}
    | (*% @format(arg) arg + "ptr" *)
      PTRty of reifiedTy
    | (*% @format "real" *)
      REAL64ty
    | (*% @format "real32" *)
      REAL32ty
    | (*% @format "label" *)
      RECORDLABELty 
    | (*% @format(arg) arg + "RecordLabel.Map.map" *)
      RECORDLABELMAPty of reifiedTy
    | (*% 
        @format(ty tys) 
         !N0{ 2[1 tys:recordTy(ty) ] }
       *)
      RECORDty of reifiedTy RecordLabel.Map.map
    | (*% @format(arg) arg + "ref" *)
      REFty of reifiedTy
    | (*% @format(arg) arg + "SEnv.map" *)
      SENVMAPty of reifiedTy
    | (*% @format "string" *)
      STRINGty
    | (*% @format "void" *)
      VOIDty
    | (*% @format "?X" *)
      TYVARty
    | (*% @format "unit" *)
      UNITty 
    | (*% @format(arg) arg + "vector" *)
      VECTORty of reifiedTy
    | (*% @format "word" *)
      WORD32ty
    | (*% @format "word8" *)
      WORD8ty
    | (*% @format "word16" *)
      WORD16ty
    | (*% @format "word64" *)
      WORD64ty

  withtype conSet = 
      (*% 
         @format(tyOpt tys) 
         !N0{ "("  2[1 tys(tyOpt)() ] 1 ")" }
         @format:tyOpt(ty opt)
           opt(ty)(+"of"+)
       *)
       (reifiedTy option) SEnv.map

  (*%  *)
  (*%  @prefix toJSON_ *)
  datatype void
    = (*%
       * @format "void"
       *)
      (*%
       * @prefix toJSON_ 
       * @format "void"
       *)
      void

  fun reifiedTyToString reifiedTy =
      let
        val f = format_reifiedTy reifiedTy
        val s = SMLFormat.prettyPrint nil f
      in
         s
      end

  fun printTy ty = print (reifiedTyToString ty)

  (* offsets *)
  val charSize = 0w1
  val int16Size = 0w2
  val int64Size = 0w8
  val int8Size = 0w1
  val intSize = 0w4
  val ptrSize = SMLSharp_Builtin.Dynamic.sizeToWord _sizeof(boxed)
  val real32Size = 0w4
  val realSize = 0w8
  val tagSize = 0w4
  val word16Size = 0w2
  val word32Size = 0w4
  val word64Size = 0w8
  val word8Size = 0w1
  val wordSize = 0w4
  fun sizeOf reifiedTy = 
      case reifiedTy of
        ARRAYty reifiedTy => ptrSize
      | BOOLty => intSize
      | BOTTOMty => intSize
      | BOXEDty => ptrSize
      | BOUNDVARty BoundTypeVarIDid => Undetermined "BOUNDVARty"
      | CHARty => charSize
      | CODEPTRty => ptrSize
      | CONSTRUCTty {longsymbol, id, args, conSet, layout, size} => Word.fromInt size
      | DATATYPEty {longsymbol, id, args, layout, size} => Word.fromInt size
      | DUMMYty {boxed, size} => size
      | EXISTty {boxed, size = SOME size, id} => size
      | EXISTty {boxed, size = NONE, id} => Undetermined "EXISTty"
      | DYNAMICty _ => ptrSize
      | ERRORty =>  Undetermined "ERRORty"
      | EXNTAGty => ptrSize
      | EXNty  => ptrSize
      | FUNMty _  => ptrSize
      | IENVMAPty _ => ptrSize
      | INT16ty => int16Size
      | INT64ty => int64Size
      | INT8ty => int8Size
      | INTERNALty => Undetermined "INTERNALty"
      | INTINFty => ptrSize
      | INT32ty => intSize
      | LISTty reifiedTy => ptrSize
      | OPAQUEty {size,...} => Word.fromInt size
      | OPTIONty reifiedTy => ptrSize
      | POLYty {boundenv, body} => sizeOf body
      | PTRty reifiedTy  => ptrSize
      | REAL32ty  => real32Size
      | REAL64ty => realSize
      | RECORDLABELty => ptrSize
      | RECORDLABELMAPty _ => ptrSize
      | RECORDty reifiedTyLabelMap => ptrSize
      | REFty reifiedTy => ptrSize
      | SENVMAPty _ => ptrSize
      | STRINGty => ptrSize
      | TYVARty => Undetermined "TYVARty"
      | UNITty => intSize
      | VECTORty reifiedTy => ptrSize
      | VOIDty => intSize
      | WORD16ty => word16Size
      | WORD64ty => word64Size
      | WORD8ty => word8Size
      | WORD32ty => word32Size

  fun isGroundTy reifiedTy =
      case reifiedTy of
      ARRAYty reifiedTy => isGroundTy reifiedTy
    | BOOLty => true
    | BOTTOMty => false
    | BOUNDVARty _  => false
    | BOXEDty => false
    | CHARty => true
    | CODEPTRty => false
    | CONSTRUCTty _ => false
    | DATATYPEty _ => false
    | DUMMYty _ => false
    | DYNAMICty _ => false
    | ERRORty => false
    | EXISTty _ => false
    | EXNTAGty => false
    | EXNty => false
    | FUNMty _ => false
    | IENVMAPty _ => false
    | INT16ty => true
    | INT32ty => true
    | INT64ty => true
    | INT8ty => true
    | INTERNALty => false
    | INTINFty => true
    | LISTty reifiedTy => isGroundTy reifiedTy
    | OPAQUEty _ => false
    | OPTIONty reifiedTy => isGroundTy reifiedTy
    | POLYty _ => false
    | PTRty _ => false
    | REAL32ty => true
    | REAL64ty => true
    | RECORDLABELMAPty _ => false
    | RECORDLABELty  => true
    | RECORDty reifiedTyRecordLabelMapmap => List.all isGroundTy (RecordLabel.Map.listItems reifiedTyRecordLabelMapmap)
    | REFty reifiedTy => isGroundTy reifiedTy
    | SENVMAPty _ => false
    | STRINGty => true
    | TYVARty => false
    | UNITty  => true
    | VECTORty _ => false
    | VOIDty => false
    | WORD16ty => true
    | WORD32ty => true
    | WORD64ty => true
    | WORD8ty => true

  fun isBoxed reifiedTy = 
      case reifiedTy of
        ARRAYty reifiedTy => true
      | BOOLty => false
      | BOTTOMty => false
      | BOUNDVARty BoundTypeVarIDid => true
      | BOXEDty => true
      | CHARty => false
      | CODEPTRty => false
      | CONSTRUCTty {longsymbol, id, args, conSet, layout, size} => isBoxedLayout layout
      | DATATYPEty {longsymbol, id, args, layout, size} => isBoxedLayout layout
      | DUMMYty {boxed, size} => boxed
      | DYNAMICty _ => true
      | ERRORty =>  false
      | EXISTty {boxed = SOME boxed, size, id} => boxed
      | EXISTty {boxed = NONE, size, id} => Undetermined "EXISTty"
      | EXNTAGty => true
      | EXNty  => true
      | FUNMty _  => true
      | IENVMAPty _ => true
      | INT16ty => false
      | INT32ty => false
      | INT64ty => false
      | INT8ty => false
      | INTERNALty => Undetermined "INTERNALty"
      | INTINFty => true
      | LISTty reifiedTy => true
      | OPAQUEty {size,...} => true
      | OPTIONty reifiedTy => true
      | POLYty {boundenv, body} => true
      | PTRty reifiedTy  => false
      | REAL32ty  => false
      | REAL64ty => false
      | RECORDLABELMAPty _ => true
      | RECORDLABELty => false
      | RECORDty reifiedTyLabelMap => true
      | REFty reifiedTy => true
      | SENVMAPty _ => true
      | STRINGty => true
      | TYVARty => Undetermined "TYVARty"
      | UNITty => false
      | VECTORty reifiedTy => true
      | VOIDty => false
      | WORD16ty => false
      | WORD32ty =>  false
      | WORD64ty =>  false
      | WORD8ty =>  false

  fun reifiedTyEq' (ty1, ty2) =
      let
        exception NotEQ
        val emptyEquivEnv = BoundTypeVarID.Map.empty
        val emptyIdEnv = IEnv.empty
        fun extendEquivEnv (btvenv1, btvenv2) equivEnv =
            ListPair.foldlEq 
              (fn (i, j, map) => BoundTypeVarID.Map.insert(map, i, j))
              equivEnv
              (BoundTypeVarID.Map.listKeys btvenv1,
               BoundTypeVarID.Map.listKeys btvenv2)
            handle ListPair.UnequalLengths => equivEnv
        fun btvIdEq equivEnv (id1, id2) = 
            BoundTypeVarID.eq(id1, id2) 
            orelse
            case BoundTypeVarID.Map.find(equivEnv, id1) of
              SOME id3 => BoundTypeVarID.eq(id3, id2) 
            | NONE => 
              (case BoundTypeVarID.Map.find(equivEnv, id2) of
                 SOME id4 => BoundTypeVarID.eq(id1, id4) 
               | NONE => false)
        fun eqList equivEnv idEnv (L1,L2) =
            foldl 
            (fn ((ty1,ty2), idEnv) => eq equivEnv idEnv (ty1,ty2))
            idEnv
            (ListPair.zip (L1,L2))
        and eq equivEnv idEnv (ty1,ty2) =
            case (ty1,ty2) of
              (EXISTty {id=id1,...}, EXISTty{id=id2, ...}) =>
              if id1 <> id2 then raise NotEQ else idEnv 
            | (EXISTty {id=id1,boxed, size}, _) =>
              (case IEnv.find(idEnv, id1) of
                 NONE =>
                 if eqOpt boxed (isBoxed ty2) andalso eqOpt size (sizeOf ty2)
                 then IEnv.insert(idEnv, id1, ty2)
                 else raise NotEQ
               | SOME ty => eq equivEnv idEnv (ty, ty2))
            | (_, EXISTty {id=id2,boxed, size}) =>
              (case IEnv.find(idEnv, id2) of
                 NONE => 
                 if eqOpt boxed (isBoxed ty1) andalso eqOpt size (sizeOf ty1)
                 then IEnv.insert(idEnv, id2, ty1)
                 else raise NotEQ
               | SOME ty => eq equivEnv idEnv (ty1, ty))
            | (ARRAYty ty1, ARRAYty ty2) => eq equivEnv idEnv (ty1, ty2)
            | (BOOLty, BOOLty) => idEnv
            | (BOTTOMty, BOTTOMty) => idEnv
            | (BOXEDty, BOXEDty) => idEnv
            | (BOUNDVARty id1, BOUNDVARty id2) => 
              if btvIdEq equivEnv (id1, id2) then idEnv
              else raise NotEQ
            | (CHARty, CHARty) => idEnv
            | (CODEPTRty, CODEPTRty) => idEnv
            | (CONSTRUCTty {id=id1, args=args1,...}, CONSTRUCTty {id=id2, args=args2,...})
              => if TypID.eq (id1, id2) then eqList equivEnv idEnv (args1, args2)
                 else raise NotEQ
            | (DATATYPEty  {id=id1, args=args1,...}, DATATYPEty {id=id2, args=args2,...}) 
              => if TypID.eq (id1, id2) then eqList equivEnv idEnv (args1, args2)
                 else raise NotEQ
            | (DYNAMICty ty1, DYNAMICty ty2)  => eq equivEnv idEnv (ty1, ty2)
            | (ERRORty, ERRORty)  => idEnv
            | (EXNTAGty, EXNTAGty) => idEnv
            | (EXNty, EXNty) => idEnv
            | (FUNMty ([arg1], ty1), FUNMty ([arg2], ty2)) => 
              eqList equivEnv idEnv ([arg1,ty1], [arg2,ty2])
            | (IENVMAPty ty1, IENVMAPty ty2) => eq equivEnv idEnv (ty1, ty2)
            | (INT32ty, INT32ty) => idEnv
            | (INT16ty, INT16ty) => idEnv
            | (INT64ty, INT64ty) => idEnv
            | (INT8ty, INT8ty) => idEnv
            | (INTERNALty, INTERNALty) => idEnv
            | (INTINFty, INTINFty) => idEnv
            | (LISTty  ty1, LISTty  ty2) => eq equivEnv idEnv (ty1, ty2)
            | (OPAQUEty {id=id1, args=args1,...}, OPAQUEty {id=id2, args=args2,...})
              => if TypID.eq (id1, id2) then eqList equivEnv idEnv (args1, args2)
                 else raise NotEQ
            | (OPTIONty ty1, OPTIONty ty2) => eq equivEnv idEnv (ty1, ty2)
            | (POLYty {boundenv=benv1, body=ty1}, POLYty {boundenv=benv2, body=ty2})
              => eq (extendEquivEnv (benv1, benv2) equivEnv) idEnv (ty1, ty2)
            | (PTRty ty1, PTRty ty2) => eq equivEnv idEnv (ty1, ty2)
            | (REAL64ty, REAL64ty) => idEnv
            | (REAL32ty, REAL32ty) => idEnv
            | (RECORDty map1, RECORDty map2) => 
              RecordLabel.Map.foldl
                (fn ((SOME ty1, SOME ty2), idEnv) => eq equivEnv idEnv (ty1,ty2)
                  | _ => raise NotEQ
                )
                idEnv
                (RecordLabel.Map.mergeWith SOME (map1, map2))
            | (REFty ty1, REFty ty2)  => eq equivEnv idEnv (ty1, ty2)
            | (SENVMAPty ty1, SENVMAPty ty2) => eq equivEnv idEnv (ty1, ty2)
            | (STRINGty, STRINGty) => idEnv
            | (VOIDty, VOIDty) => idEnv
            | (TYVARty, TYVARty) => idEnv
            | (UNITty , UNITty) => idEnv
            | (VECTORty ty1, VECTORty ty2)  => eq equivEnv idEnv (ty1, ty2)
            | (WORD32ty, WORD32ty) => idEnv
            | (WORD16ty, WORD16ty) => idEnv
            | (WORD64ty, WORD64ty) => idEnv
            | (WORD8ty, WORD8ty) => idEnv
            | _ => raise NotEQ
      in
        SOME (eq emptyEquivEnv emptyIdEnv (ty1, ty2))
        handle NotEQ => NONE
      end
  fun reifiedTyEq tys = isSome (reifiedTyEq' tys)

  val emptyConSet = SEnv.empty : conSet
  fun conSetToString conSet =
      SMLFormat.prettyPrint nil (format_conSet conSet)
  fun conSetEq (x:conSet, y:conSet) = 
      let
        fun reifiedTyOptEq (NONE, NONE) = true
          | reifiedTyOptEq (SOME a, SOME b) = reifiedTyEq (a,b)
          | reifiedTyOptEq _ = false
      in
        SEnv.isEmpty
          (SEnv.mergeWith 
             (fn (SOME a, SOME b) => if reifiedTyOptEq (a, b) then NONE else SOME (SOME a,SOME b)
               | (SOME a, NONE) => SOME (SOME a, NONE)
               | (NONE, SOME b) => SOME (NONE, SOME b)
               | (NONE, NONE) => NONE
             )
             (x,y)
          )
      end

  fun mkConSet stringReifiedTyOptlist =
      foldl
        (fn ((string, tyOpt), map) =>
            SEnv.insert
              (map, string, tyOpt))
        emptyConSet
        stringReifiedTyOptlist

  (*%
     @formatter(TypID.Map.map) TermPrintUtils.formatTypIDMap
  *)
  type conSetEnv = 
      (*% 
         @format(conset map) 
         !N0{
           "{"
              2[1 map(conset)("=>") ]
            1
           "}"
         }
       *)
       conSet TypID.Map.map
  val emptyConSetEnv = TypID.Map.empty : conSetEnv
  fun conSetEnvToString conSetEnv =
      SMLFormat.prettyPrint nil (format_conSetEnv conSetEnv)
  fun conSetEnvEq (conSetMap1, conSetMap2) =
      TypID.Map.eq conSetEq (conSetMap1, conSetMap2)
  fun lookUpConSet (conSetEnv, id) = 
      case TypID.Map.find(conSetEnv, id) of
        NONE => 
        (
         print "lookUpConSet\n";
         print (conSetEnvToString  conSetEnv);
         raise ConSetNotFound
        )
      | SOME conSet => conSet
  fun insertConSet (conSetEnv, id, conSet) =
      TypID.Map.insert(conSetEnv, id, conSet)

  val globalConSetEnv = ref TypID.Map.empty : conSetEnv ref
  fun resetGlobalConSetEnv () = globalConSetEnv := TypID.Map.empty
  fun getGlobalConSetEnv () = !globalConSetEnv

  fun findConSet id = TypID.Map.find (!globalConSetEnv, id)

  fun setConSet (id, conSet) =
       globalConSetEnv:= insertConSet (!globalConSetEnv, id, conSet)

  (*%
    @formatter(NonEmptyTypIDMap) TermPrintUtils.formatNonEmptyTypIDMap
   *)
  type tyRep = 
       (*%
          @format({conSetEnv, reifiedTy})
           "let"
             2[+1 conSetEnv:NonEmptyTypIDMap()(conSetEnv)]
            +1
            "in"
             2[+1 reifiedTy]
            +1 
            "end"
        *)
       {conSetEnv: conSetEnv, reifiedTy : reifiedTy}

  fun tyRepToString tyRep =
      SMLFormat.prettyPrint nil (format_tyRep tyRep)
  fun tyRepEq ({conSetEnv=env1, reifiedTy=ty1},{conSetEnv=env2, reifiedTy=ty2}) =
      conSetEnvEq (env1, env2) andalso reifiedTyEq (ty1, ty2)

  fun applySubst subst ty =
      let
        val apply = applySubst subst
      in
        case ty of
          BOUNDVARty id => 
          (case BoundTypeVarID.Map.find(subst, id) of
             NONE => ty | SOME newTy => newTy)
        | IENVMAPty reifiedTy => IENVMAPty (apply reifiedTy)
        | LISTty reifiedTy => LISTty (apply reifiedTy)
        | ARRAYty reifiedTy => ARRAYty (apply reifiedTy)
        | VECTORty reifiedTy => VECTORty (apply reifiedTy)
        | OPTIONty reifiedTy => OPTIONty (apply reifiedTy)
        | REFty reifiedTy => REFty (apply reifiedTy)
        | RECORDty reifiedTyMap =>
          RECORDty (RecordLabel.Map.map apply reifiedTyMap)
        | DATATYPEty {longsymbol, id, args, layout, size} =>
          DATATYPEty {longsymbol=longsymbol, id=id, args=map apply args, layout=layout, size=size}
        | POLYty {boundenv, body} =>
          POLYty {boundenv=boundenv, body = apply body}
        | SENVMAPty reifiedTy => SENVMAPty (apply reifiedTy)
        | _ => ty
      end

  fun instantiate (ty as (POLYty {boundenv, body}), args) =
      let
        val idList = BoundTypeVarID.Map.listKeys boundenv
        val idTyPairs = 
            if length args = length idList then ListPair.zip (idList, args)
            else 
              (print "instantiate arity\n";
               print (reifiedTyToString ty);
               print "\n";
               map (fn x => print (reifiedTyToString x ^ "\n")) args;
              raise InstantiateFail
              )
        val subst = foldr
                    (fn ((id,ty), newBoundEnv) =>
                        BoundTypeVarID.Map.insert(newBoundEnv, id, ty))
                    BoundTypeVarID.Map.empty
                    idTyPairs
      in
        applySubst subst body
      end
    | instantiate (ty, nil) =  ty
    | instantiate (ty, args) = 
      (print "instantiate type case\n";
       print (reifiedTyToString ty);
       print "\n";
       map (fn x => print (reifiedTyToString x ^ "\n")) args;
       raise InstantiateFail
      )

  fun getConSet {reifiedTy = DATATYPEty {longsymbol, id, args, layout, size}, conSetEnv} =
      let
        val conSet = lookUpConSet (conSetEnv, id)
      in
        SEnv.map
        (fn NONE => NONE
          | SOME ty => SOME (instantiate (ty, args)))
        conSet
      end
    | getConSet _ = raise GetConSetFail

  fun getConstructTy (tyRep as {reifiedTy = DATATYPEty {longsymbol, id, args, layout, size}, conSetEnv}) = 
      let
        val conSet = getConSet tyRep
      in
        {conSetEnv = conSetEnv,
         reifiedTy = CONSTRUCTty {longsymbol = longsymbol, id = id, args = args, conSet = conSet, layout=layout, size=size}}
      end
    | getConstructTy tyRep = tyRep

  fun stringReifiedTyListToRecordTy stringReifiedTyList =
      RECORDty
        (foldr
           (fn ((string, reifiedTy), labelMap) => 
               RecordLabel.Map.insert(labelMap, RecordLabel.fromString string, reifiedTy))
           RecordLabel.Map.empty
           stringReifiedTyList)

  fun stringReifiedTyOptionListToConSet stringReifiedTyOptionList =
      foldr
      (fn ((string, reifiedTyOpt), conSet) =>
          SEnv.insert(conSet, string, reifiedTyOpt))
      SEnv.empty
      stringReifiedTyOptionList

  fun typIdConSetListToConSetEnv typIdConSetList =
      foldr
      (fn ((typId, conSet), conSetEnv) =>
          TypID.Map.insert(conSetEnv, typId, conSet))
      TypID.Map.empty
      typIdConSetList

  fun btvIdBtvIdListToBoundenv btvIdBtvIdList =
      foldr
      (fn ((btvid1, btvid2), boundenv) =>
          BoundTypeVarID.Map.insert(boundenv, btvid1, btvid2))
      BoundTypeVarID.Map.empty 
      btvIdBtvIdList
      
  fun boundenvReifiedTyToPolyTy boundenv reifiedTy =
      POLYty {boundenv = boundenv, body = reifiedTy}

  fun makeDummyTy boxed size =
      DUMMYty {boxed = boxed, size = size}

  fun makeExistTy boxed size id =
      EXISTty {boxed = boxed, size = size, id = id}
      
  fun makeFUNMty reifiedTyList reifiedTy =
      FUNMty (reifiedTyList, reifiedTy)
      
  fun stringIntListToTagMap stringIntList =
      let
        val tagMap = 
            foldl (fn ((s, i), tagMap) => SEnv.insert(tagMap, s, i))
                  SEnv.empty
                  stringIntList
      in
        tagMap
      end

  fun stringIntListToTagMap stringIntList =
      foldl (fn ((s, i), tagMap) => SEnv.insert(tagMap, s, i))
            SEnv.empty
            stringIntList
      
  fun tagMapToTagMapRecord tagMap = {tagMap = tagMap}

  fun tagMapStringToTagMapNullNameRecord tagMap nullName =
      {tagMap = tagMap, nullName=nullName}
      
  fun stringToFalseNameRecord string = {falseName = string}

  fun boolToWrapRecord bool = {wrap = bool}

  fun TyRep conSetEnv reifiedTy =
      {conSetEnv = conSetEnv, reifiedTy = reifiedTy}

  fun MergeConSetEnvWithTyRepList conSetEnv tyRepList =
      let
        fun mergeConSet ({conSetEnv = conSet1, reifiedTy}, conSet2) =
            TypID.Map.mergeWith 
            (fn (x as SOME a, _) => x 
              | (NONE, y) => y)
            (conSet1, conSet2) 
        val conSetEnv =foldl mergeConSet conSetEnv tyRepList
      in
        conSetEnv
      end
  fun TyRepToReifiedTy {conSetEnv, reifiedTy} = reifiedTy

  fun longsymbolIdArgsLayoutListToDatatypeTy longsymbol id args layout size =
      DATATYPEty {longsymbol=longsymbol, id = id, args = args, layout=layout, size = size}

  fun longsymbolIdArgsToOpaqueTy longsymbol id args size boxed =
      OPAQUEty {longsymbol=longsymbol, id = id, args = args, size = size, boxed=boxed}

  fun makePos true _ _ _ _ _ _ = Loc.NOPOS
    | makePos false isStdPath NONE line col pos gap =
      Loc.POS {source = Loc.INTERACTIVE, line = line, col = col,
               pos = pos, gap = gap}
    | makePos false isStdPath (SOME name) line col pos gap =
      Loc.POS
        {source = Loc.FILE (if isStdPath then Loc.STDPATH else Loc.USERPATH,
                            Filename.fromString name),
         line = line,
         col = col,
         pos = pos,
         gap = gap}

  fun isBaseTy reifiedTy =
      case reifiedTy of
      ARRAYty reifiedTy => false
    | BOOLty => true
    | BOTTOMty => false
    | BOUNDVARty _  => false
    | BOXEDty => false
    | CHARty => true
    | CODEPTRty => false
    | CONSTRUCTty _ => false
    | DATATYPEty _ => false
    | DUMMYty _ => false
    | DYNAMICty _ => false
    | ERRORty => false
    | EXISTty _ => false
    | EXNTAGty => false
    | EXNty => false
    | FUNMty _ => false
    | IENVMAPty _ => false
    | INT16ty => true
    | INT32ty => true
    | INT64ty => true
    | INT8ty => true
    | INTERNALty => false
    | INTINFty => true
    | LISTty reifiedTy =>  false
    | OPAQUEty _ => false
    | OPTIONty reifiedTy =>  false
    | POLYty _ => false
    | PTRty _ => false
    | REAL32ty => true
    | REAL64ty => true
    | RECORDLABELMAPty _ => false
    | RECORDLABELty  => true
    | RECORDty reifiedTyRecordLabelMapmap =>  false
    | REFty reifiedTy =>  false
    | SENVMAPty _ => false
    | STRINGty => true
    | TYVARty => false
    | UNITty  => true
    | VECTORty _ => false
    | VOIDty => false
    | WORD16ty => true
    | WORD32ty => true
    | WORD64ty => true
    | WORD8ty => true

end
